und
Ja, dann fangen wir jetzt einfach mal an würde ich sagen
Wenn er noch kommt dann kriegt er schon
Muss ich jetzt wieder auf englisch wechseln okay
Für den Rekord
Alles klar, also wir beginnen
So jetzt gehen wir
von Modellverfahren weg für ein while
und
wie ihr wahrscheinlich in der
Lektur bemerkt, wir machen
Formelanalysen
von beherrschten Programmen
Also
die Tool, die wir
verwenden, ist fromAC
und ich habe euch alle
am Anfang dieses Tutorials
zu installieren
bereits, also
ich hoffe, dass alle es jetzt
installiert haben
aber ich habe euch
am Anfang nicht gesagt, was fromAC ist
und was wir es für
verwenden werden
also fromAC ist
eigentlich kein Tool
wie so, aber
es ist eine Kollektion von Tools
es ist ein Framework für
Statistikanalysen von C-Koden
und Statistikanalysen
enthält Dinge wie
Wertanalysen, die ihr auch
von fromAC machen könnt
das bedeutet, dass ihr eure Kode
und einige Variablen in dem
Kode schauen könnt
und an jedem Punkt
wo dieser Variabel
erwähnt wird, kann man
in fromAC zum Beispiel klicken
und eine Wertanalysen erfolgen
und es sagt, welchen
Kontext
dieser Variabel
überhaupt haben kann
also es analysiert
den Kode und sagt, dass
Presenters
Zugänglich über
Offener Zugang
Dauer
00:53:43 Min
Aufnahmedatum
2016-12-02
Hochgeladen am
2019-04-11 03:29:03
Sprache
en-US
In the first part of the course, we will engage in the formal verification of reactive systems. Students learn the syntax and semantics of the temporal logics LTL, CTL, and CTL* and their application in the specification of e.g. safety and liveness properties of systems. Simple models of systems are designed and verified using model checkers and dedicated frameworks for asynchronous and synchronous reactive systems, and the algorithms working in the background are explained.
The second part of the course focuses on functional correctness of programs; more precisely, we discuss the theory of pre- and postconditions, Hoare triples, loop invariants, and weakest (liberal) preconditions, in order to introduce automatised correctness proofs using the Hoare calculus.
Students are going to acquire the following competences:
Wissen- Reproduce the definition of syntax and semantics of temporal logics LTL, CTL, and CTL*.
-
Reproduce the definition of semantics of a simple programming languages like IMP, with special focus on axiomatic semantics (Hoare rules).
-
Explain how CTL can be characterised in terms of fixpoints.
-
model checking
-
specification and verification of reactive systems,
-
verification of functional correctness or memory safety of simple programs.
- Choose the optimal tool for a given verification or specification problem.
-
Differentiate between safety and liveness properties.